mere propositions

mere propositions(単命題？、単なる命題？)

ChatGPTによる訳は単命題

ホモトピー型理論を調べたときに出てきた

HoTTではh-propositionsとも呼ばれる？

h-level 1の型(types of h-level 1)

homotopy (−1)-types

n-truncationの分類では(-1)-truncated objects

高次元圏での対応: (-1)-groupoid

定義

型$ P が単命題(mere proposition)とは任意の$ x,y: P について$ x = y である

型$ P が型宇宙$ \mathscr{U} の型であることを$ P : \mathscr{U} と表す

$ \mathrm{isProp}(P) :\equiv \prod_{x,y:P} (x = y)

参考